not(not(x)) → x
not(or(x, y)) → and(not(not(not(x))), not(not(not(y))))
not(and(x, y)) → or(not(not(not(x))), not(not(not(y))))
↳ QTRS
↳ DependencyPairsProof
not(not(x)) → x
not(or(x, y)) → and(not(not(not(x))), not(not(not(y))))
not(and(x, y)) → or(not(not(not(x))), not(not(not(y))))
NOT(or(x, y)) → NOT(not(not(y)))
NOT(and(x, y)) → NOT(not(not(x)))
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(not(not(x)))
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(not(not(y)))
NOT(or(x, y)) → NOT(not(y))
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(not(x))
NOT(and(x, y)) → NOT(not(y))
NOT(and(x, y)) → NOT(not(x))
NOT(or(x, y)) → NOT(y)
not(not(x)) → x
not(or(x, y)) → and(not(not(not(x))), not(not(not(y))))
not(and(x, y)) → or(not(not(not(x))), not(not(not(y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
NOT(or(x, y)) → NOT(not(not(y)))
NOT(and(x, y)) → NOT(not(not(x)))
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(not(not(x)))
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(not(not(y)))
NOT(or(x, y)) → NOT(not(y))
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(not(x))
NOT(and(x, y)) → NOT(not(y))
NOT(and(x, y)) → NOT(not(x))
NOT(or(x, y)) → NOT(y)
not(not(x)) → x
not(or(x, y)) → and(not(not(not(x))), not(not(not(y))))
not(and(x, y)) → or(not(not(not(x))), not(not(not(y))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT(or(x, y)) → NOT(not(not(y)))
NOT(and(x, y)) → NOT(not(not(x)))
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(not(not(x)))
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(not(not(y)))
NOT(or(x, y)) → NOT(not(y))
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(not(x))
NOT(and(x, y)) → NOT(not(y))
NOT(and(x, y)) → NOT(not(x))
NOT(or(x, y)) → NOT(y)
The value of delta used in the strict ordering is 1/16.
POL(NOT(x1)) = (1/4)x_1
POL(not(x1)) = x_1
POL(or(x1, x2)) = 1/4 + (4)x_1 + (2)x_2
POL(and(x1, x2)) = 1/4 + (4)x_1 + (2)x_2
not(not(x)) → x
not(or(x, y)) → and(not(not(not(x))), not(not(not(y))))
not(and(x, y)) → or(not(not(not(x))), not(not(not(y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
not(not(x)) → x
not(or(x, y)) → and(not(not(not(x))), not(not(not(y))))
not(and(x, y)) → or(not(not(not(x))), not(not(not(y))))